/* @LICENSE(NICTA_CORE) */

#ifndef __LIBSEL4_ARCH_SYSCALLS_H
#define __LIBSEL4_ARCH_SYSCALLS_H

#include <stdint.h>

static inline void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo msgInfo)
{
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysSend),
          "b" (dest),
          "S" (msgInfo.raw),
          "D" (seL4_GetMR(0)),
          "c" (seL4_GetMR(1))
        : "%edx"
    );
}

static inline void
__seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo msgInfo,
        seL4_Word *mr0, seL4_Word *mr1)
{
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysSend),
          "b" (dest),
          "S" (msgInfo.raw),
          "D" (mr0 != NULL ? *mr0 : 0),
          "c" (mr1 != NULL ? *mr1 : 0)
        : "%edx"
    );
}

static inline void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo msgInfo)
{
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysNBSend),
          "b" (dest),
          "S" (msgInfo.raw),
          "D" (seL4_GetMR(0)),
          "c" (seL4_GetMR(1))
        : "%edx"
    );
}

static inline void
__seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo msgInfo,
        seL4_Word *mr0, seL4_Word *mr1)
{
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysNBSend),
          "b" (dest),
          "S" (msgInfo.raw),
          "D" (mr0 != NULL ? *mr0 : 0),
          "c" (mr1 != NULL ? *mr1 : 0)
        : "%edx"
    );
}

static inline void
seL4_Reply(seL4_MessageInfo msgInfo)
{
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysReply),
          "S" (msgInfo.raw),
          "D" (seL4_GetMR(0)),
          "c" (seL4_GetMR(1))
        : "%ebx", "%edx"
    );
}

static inline void
__seL4_ReplyWithMRs(seL4_MessageInfo msgInfo,
        seL4_Word *mr0, seL4_Word *mr1)
{
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysReply),
          "S" (msgInfo.raw),
          "D" (mr0 != NULL ? *mr0 : 0),
          "c" (mr1 != NULL ? *mr1 : 0)
        : "%ebx", "%edx"
    );
}

static inline void
seL4_Notify(seL4_CPtr dest, seL4_Word msg)
{
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysSend),
          "b" (dest),
          "S" ((seL4_MessageInfo){{ .length = 1 }}.raw),
          "D" (msg)
        : "%ecx", "%edx"
    );
}

static inline seL4_MessageInfo
seL4_Wait(seL4_CPtr src, seL4_Word* sender)
{
    seL4_MessageInfo info;
    seL4_Word badge;
    seL4_Word mr0;
    seL4_Word mr1;
    
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "movl %%ebp, %%ecx \n"
        "popl %%ebp        \n"
        :
          "=b" (badge),
          "=S" (info.raw),
          "=D" (mr0),
          "=c" (mr1)
        : "a" (seL4_SysWait),
          "b" (src)
        : "%edx", "memory"
    );

    seL4_SetMR(0, mr0);
    seL4_SetMR(1, mr1);

    if (sender)
        *sender = badge;

    return info;
}

static inline seL4_MessageInfo
__seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender,
        seL4_Word *mr0, seL4_Word *mr1)
{
    seL4_MessageInfo info;
    seL4_Word badge;
    seL4_Word msg0 = 0;
    seL4_Word msg1 = 0;
    
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "movl %%ebp, %%ecx \n"
        "popl %%ebp        \n"
        :
          "=b" (badge),
          "=S" (info.raw),
          "=D" (msg0),
          "=c" (msg1)
        : "a" (seL4_SysWait),
          "b" (src)
        : "%edx", "memory"
    );

    if (mr0 != NULL) { *mr0 = msg0; }
    if (mr1 != NULL) { *mr1 = msg1; }

    if (sender)
        *sender = badge;

    return info;
}

static inline seL4_MessageInfo
seL4_Poll(seL4_CPtr src, seL4_Word* sender)
{
    seL4_MessageInfo info;
    seL4_Word badge;
    seL4_Word mr0;
    seL4_Word mr1;
    
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "movl %%ebp, %%ecx \n"
        "popl %%ebp        \n"
        :
          "=b" (badge),
          "=S" (info.raw),
          "=D" (mr0),
          "=c" (mr1)
        : "a" (seL4_SysPoll),
          "b" (src)
        : "%edx", "memory"
    );

    seL4_SetMR(0, mr0);
    seL4_SetMR(1, mr1);

    if (sender)
        *sender = badge;

    return info;
}

static inline seL4_MessageInfo
seL4_Call(seL4_CPtr dest, seL4_MessageInfo msgInfo)
{
    seL4_MessageInfo info;
    seL4_Word mr0 = seL4_GetMR(0);
    seL4_Word mr1 = seL4_GetMR(1);
    
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "movl %%ebp, %%ecx \n"
        "popl %%ebp        \n"
        :
          "=S" (info.raw),
          "=D" (mr0),
          "=c" (mr1),
          "=b" (dest) /* dummy, tells GCC that ebx is clobbered */
        : "a" (seL4_SysCall),
          "b" (dest),
          "S" (msgInfo.raw),
          "D" (mr0),
          "c" (mr1)
        : "%edx", "memory"
    );

    seL4_SetMR(0, mr0);
    seL4_SetMR(1, mr1);

    return info;
}

static inline seL4_MessageInfo
__seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo msgInfo,
        seL4_Word *mr0, seL4_Word *mr1)
{
    seL4_MessageInfo info;
    seL4_Word msg0 = 0;
    seL4_Word msg1 = 0;

    if (mr0 != NULL && msgInfo.length > 0) msg0 = *mr0;
    if (mr1 != NULL && msgInfo.length > 1) msg1 = *mr1;

    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "movl %%ebp, %%ecx \n"
        "popl %%ebp        \n"
        :
          "=S" (info.raw),
          "=D" (msg0),
          "=c" (msg1),
          "=b" (dest) /* dummy, tells GCC that ebx is clobbered */
        : "a" (seL4_SysCall),
          "b" (dest),
          "S" (msgInfo.raw),
          "D" (msg0),
          "c" (msg1)
        : "%edx", "memory"
    );

    if (mr0 != NULL) { *mr0 = msg0; }
    if (mr1 != NULL) { *mr1 = msg1; }

    return info;
}

static inline seL4_MessageInfo
seL4_ReplyWait(seL4_CPtr dest, seL4_MessageInfo msgInfo, seL4_Word *sender)
{
    seL4_MessageInfo info;
    seL4_Word badge;
    seL4_Word mr0 = seL4_GetMR(0);
    seL4_Word mr1 = seL4_GetMR(1);
    
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "movl %%ebp, %%ecx \n"
        "popl %%ebp        \n"
        :
          "=b" (badge),
          "=S" (info.raw),
          "=D" (mr0),
          "=c" (mr1)
        : "a" (seL4_SysReplyWait),
          "b" (dest),
          "S" (msgInfo.raw),
          "D" (mr0),
          "c" (mr1)
        : "%edx", "memory"
    );

    seL4_SetMR(0, mr0);
    seL4_SetMR(1, mr1);

    if (sender)
        *sender = badge;

    return info;
}

static inline seL4_MessageInfo
__seL4_ReplyWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo msgInfo, seL4_Word *sender,
        seL4_Word *mr0, seL4_Word *mr1)
{
    seL4_MessageInfo info;
    seL4_Word badge;
    seL4_Word msg0 = 0;
    seL4_Word msg1 = 0;

    if (mr0 != NULL && msgInfo.length > 0) msg0 = *mr0;
    if (mr1 != NULL && msgInfo.length > 1) msg1 = *mr1;

    asm volatile (
        "pushl %%ebp       \n"
        "movl %%ecx, %%ebp \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "movl %%ebp, %%ecx \n"
        "popl %%ebp        \n"
        :
          "=b" (badge),
          "=S" (info.raw),
          "=D" (msg0),
          "=c" (msg1)
        : "a" (seL4_SysReplyWait),
          "b" (dest),
          "S" (msgInfo.raw),
          "D" (msg0),
          "c" (msg1)
        : "%edx", "memory"
    );

    if (mr0 != NULL) { *mr0 = msg0; }
    if (mr1 != NULL) { *mr1 = msg1; }

    if (sender)
        *sender = badge;

    return info;
}

static inline void
seL4_Yield(void) {
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysYield)
        : "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory"
    );
}

static inline void
seL4_DebugPutChar(char c) {
#if defined(SEL4_DEBUG_KERNEL)
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysDebugPutChar),
          "b" (c)
        : "%ecx", "%edx", "%esi", "%edi", "memory"
    );
#endif
}

static inline void
seL4_DebugHalt(void) {
#ifdef SEL4_DEBUG_KERNEL
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysDebugHalt)
        : "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory"
    );
#endif
}

static inline void
seL4_DebugSnapshot(void) {
#if defined(SEL4_DEBUG_KERNEL)
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysDebugSnapshot)
        : "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory"
    );
#endif
}

static inline void
seL4_DebugRun(void (*userfn) (void *), void* userarg) {
#if defined(SEL4_DANGEROUS_CODE_INJECTION_KERNEL)
    asm volatile (
        "pushl %%ebp       \n"
        "movl %%esp, %%ecx \n"
        "leal 1f, %%edx    \n"
        "1:                \n"
        "sysenter          \n"
        "popl %%ebp        \n"
        :
        : "a" (seL4_SysDebugRun),
          "b" (userfn),
          "S" (userarg)
        : "%ecx", "%edx", "%edi", "memory"
    );
#endif
}

#endif
